|
|
Vlastnosti čidel proudu
Čížek, Ondřej ; Bulín, Tomáš (oponent) ; Huzlík, Rostislav (vedoucí práce)
V této práci jsou popsány všechny používané čidla proudů, způsob jejich funkce a u každého čidla jsou popsány jejich vlastnosti. Dále je zde krátce popsán program LabVIEW a měření, které pomocí něho proběhlo se zaměřením na frekvenční charakteristiku a jeho vyhodnocení.
|
|
|
Nástroj pro abstraktní regulární model checking
Chalk, Matěj ; Rogalewicz, Adam (oponent) ; Hruška, Martin (vedoucí práce)
Metody formální verifikace mohou poskytnout automatizované ověření korektnosti softwaru (stavěné na matematických základech), což je velmi důležité. Jednou z těchto metod je abstraktní regulární model checking, jenž používá konečné automaty a převodníky pro reprezentaci množiny dosažitelných konfigurací, respektive jednokrokového přechodu mezi těmito konfiguracemi. Přestože tato metoda řeší obecně nerozhodnutelné problémy, umožňuje terminaci v mnoha praktických případech a navíc výrazně zmírňuje problém stavové exploze. Tohoto dosahuje urychlením výpočtu dosažitelných stavů pomocí inkrementálního zjemňování abstrakcí, k odstranění neplatných protipříkladů vzniklých nadaproximací pak slouží technika zjemňování abstrakce založená na protipříkladech. Cílem této práce je vytvořit dobře navržený nástroj pro abstraktní regulární model checking, jenž byl dosud implementován pouze v prototypech. Nový nástroj bude systémy modelovat pomocí symbolických automatů a převodníků namísto jejich (méně stručných) klasických alternativ.
|
|
|
Knihovna pro konečné automaty a převodníky
Bieliková, Michaela ; Lengál, Ondřej (oponent) ; Hruška, Martin (vedoucí práce)
Konečné automaty majú široké uplatnenie v informatike, okrem iných vo formálnej verifikácii, modelovaní systémov a spracovaní prirodzeného jazyka. Avšak modely skutočne reprezentujúce realitu bývajú veľmi komplikované a môžu byť definované nad veľkými, v niektorých prípadoch až nekonečnými, abecedami, a teda môžu obsahovať veľký počet prechodov. V týchto prípadoch nemusí byť je použitie algoritmov na prácu s konečnými automatmi efektívne. Symbolické automaty poskytujú stručnejší zápis tak, že namiesto symbolov v prechodoch používajú predikáty. Konečné prevodníky tiež majú široké uplatnenie, od ligvistiky až po formálnu verifikáciu. Symbolické prevodníky nahradzujú symboly dvojicou predikátov - jeden predikát pre vstupné symboly a jeden pre výstupné. Cieľom tejto práce je návrh knižnice pre klasické a symbolické automaty a prevodníky, ktorá bude vhodná na rýchle prototypovanie nových algoritmov.
|
|
|
Synchronous Formal Systems Based on Grammars and Transducers
Horáček, Petr ; Janoušek, Jan (oponent) ; Yamamura,, Akihito (oponent) ; Meduna, Alexandr (vedoucí práce)
This doctoral thesis studies synchronous formal systems based on grammars and transducers, investigating both theoretical properties and practical application perspectives. It introduces new concepts and definitions building upon the well-known principles of regulated rewriting and synchronization. An alternate approach to synchronization of context-free grammars is proposed, based on linked rules. This principle is extended to regulated grammars such as scattered context grammars and matrix grammars. Moreover, based on a similar principle, a new type of transducer called the rule-restricted transducer is introduced as a system consisting of a finite automaton and context-free grammar. New theoretical results regarding the generative and accepting power are presented. The last part of the thesis studies linguistically-oriented application perspectives, focusing on natural language translation. The main advantages of the new models are discussed and compared, using select case studies from Czech, English, and Japanese to illustrate.
|
|
|
Systémy převodníků
Skácel, Jiří ; Kučera, Jiří (oponent) ; Meduna, Alexandr (vedoucí práce)
Tato práce zavádí systémy zásobníkových převodníků. Základní myšlenka vychází z kooperujících distribuovaných gramatických systémů, které umožňují práci více gramatik na jednom řetězci. Převodníky spolupracují předáváním výsledků svých překladů jako vstupu pro další komponentu. Dále tato práce zkoumá jejich popisnou sílu a ekvivalenci systémů s různými počty komponent. Hlavním závěrem je pak porovnání popisné síly s Turingovými stroji a to s ohledem na jimi definovaný překlad i přijímané jazyky.
|
|
|
Improvements of the ASMA Tool for Analysis of String Manipulating Programs via Symbolic Automata
Kmenta, Martin ; Lengál, Ondřej (oponent) ; Vojnar, Tomáš (vedoucí práce)
In this work we deal with regular model checking which is a technique for analyzing programs whose state space can be infinite due to dealing with, e.g. unbounded queues, parameters, dynamically linked data structures, recursive procedures, or strings. The goal of this work was to implement improvements to the existing prototype tool ASMA implementing regular model checking over the Microsoft Automata library. We analysed the source code of ASMA and reran analyses of all available benchmark programs. We identified some bottlenecks and have tackled several of them. In particular, we integrated a library containing additional reduction algorithms into ASMA, created several new versions of the reverse concatenation operation, which tuned out to be very costly in the benchmarks, improved the command line interface of ASMA, and implemented some other optimizations for ASMA. The computation time was reduced by 90 % when analysing bigger programs.
|
|
|
Měření magnetických vlastností materiálů pomocí programu LabVIEW
Šolc, Martin ; Bulín, Tomáš (oponent) ; Huzlík, Rostislav (vedoucí práce)
V této práci je popsán program LabVIEW a jeho vývojové prostředí. Dále jsou rozebrána nejčastěji používaná čidla proudů, popsány principy jejich funkce a jejich vlastnosti. V další části práce se zabývám popisem integračních článků a jejich vlastnostmi. Poté se věnuji hysterezním křivkám feromagnetických materiálů. V praktické části bakalářské práce se zabývám měřením BH křivek pro toroidní transformátor, které jsem zrealizoval pomocí programu vytvořeném v LabVIEW, použitím digitální integrace v LabVIEW, integrace pomocí integračního RC článku a proudového čidla ITN 12-P Ultrastab. Na závěr se věnuji vyhodnocení provedeného měření.
|
|
|
Data Acquisition and Control System of Hydroelectric Power Plant Using Internet Techniques
Sattouf, Mousa ; Přikryl, Hynek (oponent) ; Richter, Aleš (oponent) ; Skalický, Jiří (vedoucí práce)
Hydropower has now become the best source of electricity on earth. It is produced due to the energy provided by moving or falling water. History proves that the cost of this electricity remains constant over the year. Because of the many advantages, most of the countries now have hydropower as the source of major electricity producer. The most important advantage of hydropower is that it is green energy, which mean that no air or water pollutants are produced, also no greenhouse gases like carbon dioxide are produced which makes this source of energy environment-friendly. It prevents us from the danger of global warming. Using internet techniques to control several hydroelectric plants has very important advantages, as reducing operating costs and the flexibility of meeting changes of energy demand occurred in consumption side. Also it is very effective to confront large disturbances of electrical grid, such as adding or removing large loads, and faults. In the other hand, data acquisition systems provides very useful information for both typical and scientific analysis, such as economical costs reducing, fault prediction systems, demand prediction, maintenance schedules, decision support systems and many other benefits. This thesis describes a generalized model which can be used to simulate a data acquisition and control system of hydroelectric power plant using MATLAB/SIMULINK and TrueTime simulink library. The plant considered consists of hydro turbine connected to synchronous generator with excitation system, and the generator is connected to public grid. Simulation of hydro turbine and synchronous generator can be done using various simulation tools, In this work, SIMULINK/MATLAB is favored over other tools in modeling the dynamics of a hydro turbine and synchronous machine. The SIMULINK program in MATLAB is used to obtain a schematic model of the hydro plant by means of basic function blocks. This approach is pedagogically better than using a compilation of program code as in other software programs .The library of SIMULINK software programs includes function blocks which can be linked and edited to model. Either Simulink Real-Time library or TrueTime library can be used to build and simulate internet and real time systems, in this thesis the TrueTime library was used.
|
|
|
Improvements of the ASMA Tool for Analysis of String Manipulating Programs via Symbolic Automata
Kmenta, Martin ; Lengál, Ondřej (oponent) ; Vojnar, Tomáš (vedoucí práce)
In this work we deal with regular model checking which is a technique for analyzing programs whose state space can be infinite due to dealing with, e.g. unbounded queues, parameters, dynamically linked data structures, recursive procedures, or strings. The goal of this work was to implement improvements to the existing prototype tool ASMA implementing regular model checking over the Microsoft Automata library. We analysed the source code of ASMA and reran analyses of all available benchmark programs. We identified some bottlenecks and have tackled several of them. In particular, we integrated a library containing additional reduction algorithms into ASMA, created several new versions of the reverse concatenation operation, which tuned out to be very costly in the benchmarks, improved the command line interface of ASMA, and implemented some other optimizations for ASMA. The computation time was reduced by 90 % when analysing bigger programs.
|
|
|
Nástroj pro abstraktní regulární model checking
Chalk, Matěj ; Rogalewicz, Adam (oponent) ; Hruška, Martin (vedoucí práce)
Metody formální verifikace mohou poskytnout automatizované ověření korektnosti softwaru (stavěné na matematických základech), což je velmi důležité. Jednou z těchto metod je abstraktní regulární model checking, jenž používá konečné automaty a převodníky pro reprezentaci množiny dosažitelných konfigurací, respektive jednokrokového přechodu mezi těmito konfiguracemi. Přestože tato metoda řeší obecně nerozhodnutelné problémy, umožňuje terminaci v mnoha praktických případech a navíc výrazně zmírňuje problém stavové exploze. Tohoto dosahuje urychlením výpočtu dosažitelných stavů pomocí inkrementálního zjemňování abstrakcí, k odstranění neplatných protipříkladů vzniklých nadaproximací pak slouží technika zjemňování abstrakce založená na protipříkladech. Cílem této práce je vytvořit dobře navržený nástroj pro abstraktní regulární model checking, jenž byl dosud implementován pouze v prototypech. Nový nástroj bude systémy modelovat pomocí symbolických automatů a převodníků namísto jejich (méně stručných) klasických alternativ.
|
host ::
RSS.